This invention relates generally to analysis of software programs such as object code, bytecode, executable code, and libraries, and, more specifically, relates to static analysis of software programs.
Computer systems have secure resources (also called “protected” resources) where security to the protected resource is important. For example, it is beneficial to control access to a network socket (e.g., an endpoint for a communication flow across a computer network), as viruses and other malicious software programs can use a socket to send and receive data, potentially without a user's knowledge. Similarly, certain operating system and other files should be similarly controlled. Therefore, it would be beneficial to determine whether a software program is allowed to access a protected resource prior to the access.
Along these lines, the Principle of Complete Mediation dictates that access to any secure resource (also called a “protected” resource) for a computer system should be preceded by an appropriate verification check. Before a protected resource (e.g., a file or socket as in traditional access control, or even a method as in Role-Based Access Control) is accessed, a system enforces security by verifying that the entities responsible for that access are sufficiently verified. Such verification can include, e.g., authentication (e.g., the entity is the entity it says it is) or authorization (e.g., the entity is allowed to access the secure resource), or both. Such entities can include the user running the system as well as system-component providers.
Modern computer systems install a special access-control enforcer for verification, commonly called the “security manager”. A problem that arises with access-control enforcement is that such enforcement is expensive. Therefore, verification systems tend to cache authorization checks.
This can lead to another problem because by the time a resource is accessed, the relevant verification check in the cache may no longer be valid, and a Time Of Check To Time Of Use (TOCTTOU) attack is possible. That is, at the time the verification, code for a software program verifies access to a first secure resource using a reference (e.g., a pointer) to the first secure resource. At the time an access is made to a secure resource using the pointer, the value of the pointer has changed and now points to a different secure resource for which authorization was not verified. It is also possible for the authorization mechanism to have not been correctly implemented and so, even when the authorization mechanism is supposed to enforce authorization for a particular resource, in reality the authorization mechanism is not doing so properly, or maybe the authorization mechanism is doing that for a resource that is not the intended one. As a consequence, a verification for the secure resource that is about to be accessed has not been performed, and such secure resource is therefore accessed without a verification check.
There are a few techniques for improving verification of access by software programs to secure resources for computer systems. The most labor intensive and least likely to produce adequate results is manual code inspection: a person checks every line of a software program for verification of access to secure resources.
Another technique is dynamic testing of the software program. This analysis involves executing the program and observing whether secure resources are accessed without verification. One problem with this technique is the technique is not conservative: a reported problem is a real problem (no false positives), but the result is potentially unsound, meaning that some real problems may not be discovered by the analysis (false negatives). For example, an access to a secure resource could be dependent on a value of a variable. Many of the values of the variable do not cause inappropriate access to a secure resource, whereas a single value of the variable may cause inappropriate access to a secure resource. A particular runtime environment may not adequately test all possible values of the variable, and therefore miss the inappropriate access to a secure resource.
In contrast to dynamic analysis of a software program, a static analysis of a software program evaluates the program statically and the program is not executed during this process. Certain models (such as call graphs and points-to graphs) may be created from the software program, based on a line-by-line interpretation of the program. Such models may be analyzed to determine information about the software program.
The inventors have realized that there are certain benefits in applying static analysis of a software program to an analysis for verification of software program access to secure resources for computer systems, especially when it comes to security analysis, in which case it is essential not to miss any security issue. Such benefits overcome the previously described problems, especially with the dynamic analysis of software programs.